package systemf;

/**
 * System F解释器主类
 * 提供便捷的API来使用System F解释器
 */
public class SystemF {
    
    private final TypeChecker typeChecker;
    private final Evaluator evaluator;
    
    public SystemF() {
        this.typeChecker = new TypeChecker();
        this.evaluator = new Evaluator();
    }
    
    /**
     * 解析并求值System F项
     */
    public Term eval(String input) {
        Parser parser = new Parser(input);
        Term term = parser.parseTerm();
        return evaluator.evaluate(term);
    }
    
    /**
     * 解析并类型检查System F项
     */
    public Type typeCheck(String input) {
        Parser parser = new Parser(input);
        Term term = parser.parseTerm();
        return typeChecker.inferType(term);
    }
    
    /**
     * 解析、类型检查并求值
     */
    public Result evalWithTypeCheck(String input) {
        Parser parser = new Parser(input);
        Term term = parser.parseTerm();
        Type type = typeChecker.inferType(term);
        Term result = evaluator.evaluate(term);
        return new Result(result, type);
    }
    
    /**
     * 添加变量到类型上下文
     */
    public void addVar(String name, Type type) {
        typeChecker.addVar(name, type);
    }
    
    /**
     * 结果类
     */
    public static class Result {
        private final Term term;
        private final Type type;
        
        public Result(Term term, Type type) {
            this.term = term;
            this.type = type;
        }
        
        public Term getTerm() {
            return term;
        }
        
        public Type getType() {
            return type;
        }
        
        @Override
        public String toString() {
            return term + " : " + type;
        }
    }
}

